the_es:ES, e':E, n:.
n<||before(e')||  firstn(n;before(e')) = before(before(e')[n])  E List 

latex

Definitions

S  T, Top, SQType(T), ij, i<j, hd(l), P  Q, Dec(P), P  Q, pred(e), WellFnd{i}(A;x,y.R(x;y)), x. t(x), {T}, firstn(n;as), l[i], ES, Unit, P  Q, P & Q, first(e), , b, b, t  ...$L, AB, A, False, ij, Prop, ||as||, as @ bs, before(e), E, t  T, (e <loc e'), P  Q, x:A. B(x),

Lemmas

es-pred-locl, es-pred wf, nat wf, es-before wf, append wf, length wf1, length wf2, length nil, assert wf, not wf, bnot wf, bool wf, es-first wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, event system wf, select wf, firstn wf, es-locl wf, es-E wf, es-locl-wellfnd, decidable int equal, length append, non neg length, length cons, select append back, top wf, first0, firstn append, firstn length, select append front